PRISM

Benchmark
Model:bluetooth v.1 (DTMC)
Parameter(s)mrec = 1
Property:time (exp-reward)
Invocation (default)
./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 bluetooth.prism bluetooth.props --property time -const mrec=1
Execution
Walltime:12.952099561691284s
Return code:0
Relative Error:0.0
Log
PRISM
=====

Version: 4.5.dev
Date: Sat Mar 14 11:34:14 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 bluetooth.prism bluetooth.props --property time -const mrec=1

Parsing model file "bluetooth.prism"...

Type:        DTMC
Modules:     receiver1 frequency1 sender_frequency replies 
Variables:   y1 receiver freq1 train1 z1 f1 t1 send freq train c rep rec 

Parsing properties file "bluetooth.props"...

1 property:
(1) "time": filter(max, R=? [ F rec=mrec ], "init")

---------------------------------------------------------------------

Model checking: "time": filter(max, R=? [ F rec=mrec ], "init")
Model constants: mrec=1

Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).

Building model...
Model constants: mrec=1

Computing reachable states...

Reachability (BFS): 50 iterations in 0.17 seconds (average 0.003360, setup 0.00)

Time for model construction: 11.299 seconds.

Type:        DTMC
States:      3411945339 (536870912 initial)
Transitions: 5035263739

Transition matrix: 14727 nodes (4 terminal), 5035263739 minterms, vars: 52r/52c

Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.

Prob0: 49 iterations in 0.28 seconds (average 0.005673, setup 0.00)

Prob1: 1 iterations in 0.00 seconds (average 0.001000, setup 0.00)

goal = 1636000575, inf = 0, maybe = 1775944764

Computing remaining rewards...
Engine: MTBDD

Iteration matrix MTBDD... [nodes=11441] [223.5 Kb]
Diagonals MTBDD... [nodes=4425] [86.4 Kb]

Starting iterations...

Jacobi: 47 iterations in 0.55 seconds (average 0.011404, setup 0.01)

Maximum value over states satisfying filter: 8229.0

There are 32768 states with (approximately) this value.
The first 10 states are displayed below. To view them all, enable verbose mode or use a print filter.
4479:(0,0,0,0,1,1,0,1,2,0,3,128,0)
4735:(0,0,0,0,1,1,0,1,2,0,5,128,0)
4991:(0,0,0,0,1,1,0,1,2,0,7,128,0)
5247:(0,0,0,0,1,1,0,1,2,0,9,128,0)
5503:(0,0,0,0,1,1,0,1,2,0,11,128,0)
5759:(0,0,0,0,1,1,0,1,2,0,13,128,0)
6015:(0,0,0,0,1,1,0,1,2,0,15,128,0)
6271:(0,0,0,0,1,1,0,1,2,1,1,128,0)
233777:(0,0,0,0,2,1,0,1,2,0,3,128,0)
234033:(0,0,0,0,2,1,0,1,2,0,5,128,0)

Time for model checking: 0.844 seconds.

Result: 8229.0 (maximum value over states satisfying filter)


Overall running time: 12.773 seconds.

---------------------------------------------------------------------

Note: There were 2 warnings during computation.